/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.sharbool;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.ASTDepthFirstReturnVisitor;
import alloy.ast.ComprehensionExpr;
import alloy.ast.DeclIter;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.Formula;
import alloy.ast.HasType;
import alloy.ast.Leaf;
import alloy.ast.LeafId;
import alloy.ast.LiteralIntExpr;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Node;
import alloy.ast.Op;
import alloy.ast.SetMultExpr;
import alloy.ast.VarCreator;
import alloy.ast.VariableExpr;
import alloy.bool.BooleanFormula;
import alloy.transl.QVarIterationInfo;
import alloy.transl.Transl;
import alloy.transl.TranslInfo;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.MultiDimIter;
import alloy.util.Util;

/**
 * Detects instances where identical {@link BooleanFormula}s would be
 * output from translating different parts of the AST.  Since our Boolean
 * formula representation can represent sharing of subformulas (it is
 * a Boolean formula DAG, not a Boolean formula tree), we can use this
 * information to make the Boolean DAG we output significantly
 * smaller by sharing identical Boolean subformulas.  Sharing means that
 * the first of the identical formulas is represented as-is, but subsequent
 * Boolean formulas identical to it are represented by a backpointer to the
 * first formula.  Thus the second and subsequent subformulas are represented
 * very compactly.
 *  <p>
 * Identical Boolean subformulas arise from Alloy formulas (AST subtrees)
 * fitting a common template.  In the simplest case, if A and B are state
 * relations, the Alloy formula "A in B", if used twice in different places
 * of the AST, translates to an identical Boolean formula in both places.
 * Similarly, the expression (A & B), if used twice in different places
 * of the AST, translates into two distinct but identical <em>arrays</em> of
 * Boolean formulas.  In sum, any two isomorphic subtrees of the AST not
 * involving any quantified variables translate to identical
 * {@link alloy.transl.Transl}ations, the corresponding {@link BooleanFormula}s
 * of which are identical and could be shared.
 * <p>
 * With quantified variables present, the situation becomes more interesting.
 * Consider three AST nodes
 *    all x: A | F(x)
 *    some y: A | F(y)
 *    { z: A | F(z) }
 *  which translate (ignoring skolemization), for scope of A being 3, into
 *    F(A0) && F(A1) && F(A3)
 *    F(A0) && F(A1) && F(A3)
 *    [ F(A0) F(A1) F(A2) ]
 *  where A0 is the singleton set consisting of atom 0 of A, etc.
 *  We'd like to generate the formula F(Ai) only once, for each i, and in other
 *  places where we would generate the same Boolean formula to backreference
 *  to the first such formula instead.
 *  <p>
 *  The visit() methods return a {@link TemplateInstance} for the visited node.
 *  <p>
 *  This visitor relies heavily on the correct operation of
 *  {@link alloy.transform.SetLeafIdsVisitor}.
 *  <p>
 *  <em>Note on terminology:</em> "Template" in this file refers to AST subtrees
 *  fitting a template, and is not Alloy's polymorphism mechanism.
 */
public class TemplateDetectVisitor extends ASTDepthFirstReturnVisitor {
    
    /////////////
    // Fields: //
    /////////////
    
    /**
     * The translator that translated the {@link Formula}.  We use it to get
     * {@link Transl}ations of {@link Node}s, as well as various other useful
     * info such as multiplicities of quantified variables.
     */
    private final TranslInfo _translator;
    
    /** For each {@link RelationType}, the {@link Template} corresponding
     to constant-valued expressions of this type.  Constant-valued meaning that they do
     not involve any relations to which Boolean variables have
     been allocated (but can involve quantified variables to which
     switchable constants have been allocated, or relations whose value
     is set to constant e.g. total orders, or {@link LiteralIntExpr}s).  They are "constant-valued"
     because their value is completely determined for any given assignment
     of quantified variables. {@link Map} from {@link RelationType} to {@link Template}. */
    private final Map _relTypeTemplate = new TreeMap();
    
    /** For each {@link LeafId} (except {@link LeafId}s for constant-valued leaves),
     the {@link Template} for {@link Node}s consisting of this leaf.
     {@link Map} from {@link LeafId} to {@link Template}. */
    private final Map _leafTemplate = new TreeMap();
    
    /** For each node, its template instance. {@link Map} from
     {@link Node} to {@link Set} of {@link TemplateInstance}s matched
     by the node. */
    private final Map _node2templateInstance = new TreeMap();
    
    /** All the {@link Template}s we find.  {@link Set} of {@link Template}. */
    private final List _allTemplates = new ArrayList();
    
    /**
     * {@link LeafId} substitution {@link Map} -- used only in {@link Template#templateDetector}
     * instances of {@link TemplateDetectVisitor}.
     * @see #_visitLeaf
     */
    private Map /* LeafId->LeafId */ _leafIdSubst = new TreeMap();
    
    /**
     * {@link LeafId}s declared in the {@link VarCreator} for whose body's template instance's argument
     * we're now determining the template.
     */
    private Set /* of LeafId */ _declaredVarIds = new TreeSet();
    
    /**
     * Whether this is an auxiliary visitor created during traversal
     * of a VarExpr arg.
     */
    private boolean _isAuxiliary;
    
    /** Whether template detection should immediately abort because the user wants to cancel the analysis. */
    private boolean _interruptInProgress;
    
    //////////////
    // Methods: //
    //////////////
    
    public TemplateDetectVisitor(TranslInfo translator_) { _translator = translator_; }
    
    /** A leaf, except for quantified variables, is its own template.
     Only {@link Node}s representing the same leaf can fit the template.
     E.g. if A$data is a relation, only {@link Node}s of them form
     A$data relation fit the same template.  For now, leaves include
     relations, univ/iden/none expressions, and integer literal constants.
     @see #_leafTemplate */
    private Object _visitLeaf(Leaf leaf_) {
        TemplateInstance templInst = new TemplateInstance(leaf_);
        _node2templateInstance.put(leaf_, Collections.singleton(templInst));
        
        LeafId leafId = leaf_.getLeafId();
        Dbg.chk(leafId, "NO LEAFID: " + leaf_.fullString() + " aux: " + _isAuxiliary);
        
        LeafId substitutedLeafId = (LeafId)_leafIdSubst.get(leafId);
        if (substitutedLeafId != null)
            leafId = substitutedLeafId;
        
        /* check if leaf_ fits a previously seen template */
        Template templ = (Template)_leafTemplate.get(leafId);
        
        if (templ == null) {
            // this is the first time we've encountered a leaf with this LeafId,
            // so establish a new template to represent leaves with this LeafId.
            _allTemplates.add(templ = new Template());
            _leafTemplate.put(leafId, templ);
        }
        templ.instances.add(templInst);
        templInst.template = templ;
        
        //      System.out.println("result for leaf node " + leaf_.fullString() + " is template "
        //                 + _allTemplates.indexOf(templInst.template) +
        //                 " with args " + templInst.args);
        
        _chkInst(templInst);
        return Collections.singleton(templInst);
    }  // _visitLeaf()
    
    /**
     * Handles constant-valued {@link Expr}essions, i.e. those whose value is
     * completely known at grounding-out time -- which means those that
     * reference only quantified variable or constant values (such as
     * fields of total orders), but do not reference any relations
     * to which we've {@link alloy.transl.BoolVarAllocator allocated}
     * any Boolean variables.  We say that all constant-valued {@link Expr}essions
     * of a given {@link RelationType} are {@link TemplateInstance instances} of
     * one {@link Template}.
     * @see #_isConstantValued
     */
    private Object _visitConstExpr(Expr constExpr_) {
        TemplateInstance templInst = new TemplateInstance(constExpr_);
        _node2templateInstance.put(constExpr_, Collections.singleton(templInst));
        
        RelationType relType = ((HasType)constExpr_).getType().toRelationType();
        // do we already have a template for constant-valued Expr nodes of type relType?
        Template templ = (Template)_relTypeTemplate.get(relType);
        if (templ == null) {
            // A new template for constant-valued nodes of this RelationType
            _allTemplates.add(templ = new Template());
            _relTypeTemplate.put(relType, templ);
        }
        templ.instances.add(templInst);
        templInst.template = templ;
        templInst.args.add(constExpr_);
        
        //      System.out.println("result for constexpr node " + constExpr_.fullString() + " is template "
        //                 + _allTemplates.indexOf(templInst.template) +
        //                 " with args " + templInst.args);
        _chkInst(templInst);
        return Collections.singleton(templInst);
    }  // _visitConstExpr()
    
    /**
     * Determine whether the value of a {@link Node} is known at grounding-out time --
     * i.e. if during grounding-out we reach this {@link Node} we known its value
     * completely.  Nodes whose {@link Transl}ations include any Boolean variables are
     * <em>not</em> constant-valued, since at grounding-time we have not yet solved
     * for the values of these Boolean variables.
     */
    private boolean _isConstantValued(Node node_) {
        if (node_ instanceof VarCreator) return false; // hack
        Transl transl = _translator.getNodeTransl(node_);
        if (transl == null) {
            //System.out.println("constant (no transl): " + node_.fullString());
            return true;
        }
        
        // if the translation of the node includes any non-constant-valued
        // boolean formulas, the node is definitely not constant-valued
        if (!transl.isConstantValued())
            return false;
        
        // if this is an auxiliary template detector, and
        // the node is a quantified variable declared in the VarCreator
        // for whose body template instance's argument we're now detecting
        // templates, the node is not constant-valued.
        if (node_ instanceof VariableExpr &&
                ((VariableExpr)node_).isQuantified &&
                _declaredVarIds.contains(((VariableExpr)node_).getLeafId()))
            return false;
        
        // otherwise, constant-valued iff children are
        if (!(node_ instanceof Leaf)) {
            for (Iterator childIter = node_.getChildren(); childIter.hasNext();) {
                Node child = (Node)childIter.next();
                if (!(node_ instanceof VarCreator && child==((VarCreator)node_).getDecls()))
                    if (!_isConstantValued(child))
                        return false;
            }
        }
        
        //System.out.println("constant: " + node_.fullString());
        return true;
    }
    
    /**
     * Determine the {@link Template} matched by the given {@link Node}.
     */
    public Object visit(Node node_) {
        if (_interruptInProgress) return null;
        
        //System.out.println("visiting node: " + node_);
        //
        // If we have already visited this node, return the template
        // we have detected.  The only way this can happen is if this
        // is a {@link VarCreatorTemplate#argTemplateDetector} visitor,
        // and two arguments of a template instance reference the same Node.
        //
        
        Set priorTemplateInstance =
            (Set)_node2templateInstance.get(node_);
        if (priorTemplateInstance != null) {
            //      System.out.println("prior for node " + node_.fullString() + " is template "
            //                 + _allTemplates.indexOf(priorTemplateInstance.template) +
            //                 " with args " + priorTemplateInstance.args);
            return priorTemplateInstance;
        }
        
        //
        // If node_ is a constant-valued expression or a leaf, these are
        // our base cases for determining what template the node_ matches,
        // and we handle such nodes in separate methods.
        //
        
        if (node_ instanceof Expr && _isConstantValued(node_))
            return _visitConstExpr((Expr)node_);
        
        if (node_ instanceof Leaf) return _visitLeaf((Leaf)node_);
        
        //
        // Not a special case -- meaning this is a non-constant-valued
        // internal AST node.
        //
        
        // For each Node in the AST, we create a TemplateInstance which
        // specifies the template matched by the Node, and the list of
        // arguments (constant-valued Nodes) with which it matches the template.
        TemplateInstance templInst = new TemplateInstance(node_);
        _node2templateInstance.put(node_, Collections.singleton(templInst));
        
        VarCreator varCreator = (node_ instanceof VarCreator) ? (VarCreator)node_ : null;
        boolean isVarCreator = (varCreator != null);
        
        Set declaredVarIds = new TreeSet();
        if (isVarCreator) {
            // compute the set of LeafIds of quantified variables declared
            // in the VarCreator
            
            for (DeclIter declIter = new DeclIter(varCreator); declIter.hasNext();) {
                declIter.next();
                declaredVarIds.add(declIter.getLeafId());
            }
        }
        
        //
        // First of all, determine the template instance
        // for each child.  We do this for all children,
        // including Op nodes.  One exception: for VarCreator nodes, we
        // do not do template detection on
        // the declarations; we do an explicit check to make sure
        // they match.  This is because the declaration structure
        // is less regular than the rest of the tree structure;
        // see alloy.ast.DeclIter for details.
        //
        List children = new ArrayList();  // node's children, minus any Decls node
        for (Iterator nodeChildIter = node_.getChildren(); nodeChildIter.hasNext();) {
            Node child = (Node)nodeChildIter.next();
            if (!(isVarCreator && child==varCreator.getDecls()))
                children.add(child);
        }
        
        TemplateInstance[] childTempl = new TemplateInstance[children.size()];
        for (int i=0; i<childTempl.length; i++) {
            Node child = (Node)children.get(i);
            childTempl[i] = _chooseInst(child.applyReturnVisitor(this));
            if (_interruptInProgress) return null;
        }
        
        //
        // Whether node_ turns out to start a new template or to
        //  match a previously seen template, the argument list
        // will be a concatenation of child argument lists
        // (unless node_ is a VarCreator).
        // Note that the argument lists generated here may be shortened
        // later in a post-processing step, _shortenTemplateArgLists .
        //
        
        List commuteArgs = null;
        if (!isVarCreator) {
            for (int i=0; i<childTempl.length; i++)
                templInst.args.addAll(childTempl[i].args);
            if (node_.numChildren() == 3 &&
                    childTempl.length == 3 &&
                    node_.childAt(1) instanceof Op &&
                    ((Op)node_.childAt(1)).isCommutative() &&
                    childTempl[0].template == childTempl[2].template) {
                commuteArgs = new ArrayList();
                commuteArgs.addAll(childTempl[2].args);
                Dbg.check(childTempl[1].args.isEmpty());
                commuteArgs.addAll(childTempl[0].args);
            }
        } else {  // isVarCreator
            TemplateInstance bodyTemplateInstance = _getInst(varCreator.getBody());
            for (Iterator argIter = bodyTemplateInstance.args.iterator(); argIter.hasNext();) {
                Expr arg = (Expr)argIter.next();
                TemplateDetectVisitor argTemplDetector = new TemplateDetectVisitor(_translator);
                argTemplDetector._declaredVarIds = declaredVarIds;
                argTemplDetector._isAuxiliary = true;
                TemplateInstance argInst =
                    _chooseInst(arg.applyReturnVisitor(argTemplDetector));
                if (_interruptInProgress) return null;
                templInst.args.addAll(argInst.args);
            }
        }
        
        boolean haveLongArg = false;
        for (int i=0; i<templInst.args.size(); i++)
            if (((HasType)templInst.args.get(i)).getType().toRelationType().numBasicTypes() > 1)
                haveLongArg = true;
            
            /* Determine which of previously seen templates
             might match node_.  Any such template will have
             children templates matched by node_'s corresponding
             children.  Above, we have determined the template
             matched by each child.  For each template we have kept
             a set of parent templates.  */
            
        boolean matchingTemplateFound = false;
        if (childTempl.length > 0) {
            /* Compute the intersection of the children's template parent sets. */
            Dbg.check(childTempl[0]);
            Dbg.check(childTempl[0].template);
            Set candidateTemplates = new TreeSet(childTempl[0].template.parents);
            for (int i=1; i<childTempl.length; i++) {
                Dbg.check(childTempl[i]);
                Dbg.check(childTempl[i].template);
                candidateTemplates.retainAll(childTempl[i].template.parents);
            }
            
            // All templates that might be matched by node_ are now
            // in candidateTemplates.
            
            // Test whether node_ matches one of the candidateTemplates.
            // It should not match more than one unless we've done something incorrectly.
            
            
            for (Iterator candIter = candidateTemplates.iterator();
            !matchingTemplateFound && candIter.hasNext();) {
                Template candTempl = (Template)candIter.next();
                TemplateInstance candTemplInst = candTempl.getAnInstance();
                Node candTemplNode = candTemplInst.node;
                
                // Rule out obvious mismatches.
                if (!candTemplNode.getClass().equals(node_.getClass())) continue;
                if (node_ instanceof Op) {
                    Op thisOp = (Op)node_;
                    Op candOp = (Op)candTemplNode;
                    if (!thisOp.equals(candOp)) continue;
                }
                if (node_ instanceof HasType &&
                        !((HasType)node_).getType().equals(((HasType)candTemplNode).getType()))
                    continue;
                if (candTempl.children.length != children.size()) continue;
                if (haveLongArg) continue;
                
                // Check whether corresponding children match.
                boolean childrenMatch = true;
                
                for (int i=0; i<childTempl.length; i++)
                    childrenMatch &= (childTempl[i].template == candTempl.children[i]);
                
                if (childrenMatch) {
                    boolean completeMatch = true;
                    if (isVarCreator) {
                        //
                        // For VarCreator node, there are additional checks.
                        //
                        
                        // check that the quantified variable declaration lists match.
                        DeclIter thisDeclIter = new DeclIter(varCreator);
                        DeclIter instDeclIter = new DeclIter((VarCreator)candTemplNode);
                        boolean foundMismatch = false;
                        Map leafIdSubst = new TreeMap();
                        while(!foundMismatch && thisDeclIter.hasNext() && instDeclIter.hasNext()) {
                            thisDeclIter.next(); instDeclIter.next();
                            MultiplicityExpr thisMult = thisDeclIter.getMultiplicity();
                            MultiplicityExpr instMult = instDeclIter.getMultiplicity();
                            foundMismatch |=
                                !thisDeclIter.getType().equals(instDeclIter.getType()) ||
                                !thisMult.isSameAs(instMult);
                            leafIdSubst.put(thisDeclIter.getLeafId(),
                                    instDeclIter.getLeafId());
                        }
                        foundMismatch |= (thisDeclIter.hasNext() || instDeclIter.hasNext());
                        
                        if (foundMismatch)
                            completeMatch = false;
                        else {  // did not find a mismatch in the declarations
                            // So, the quantified variable declaration lists are
                            // identical in node_ and candTemplNode (except for variable names):
                            // the same numbers of variables are declared, and
                            // corresponding variables have the same RelationType and multiplicity.
                            
                            // And, as we checked previously, the formula body of node_ matches
                            // the same template as the formula body of candTemplNode.
                            
                            // That still doesn't guarantee that node_ and candTemplNode match
                            // the same template.  E.g.
                            //  all x: A | F(x)
                            //      and
                            //  all y: A | F(y.next)
                            // satisfy the above conditions but do not match the same template.
                            //
                            
                            // For two VarCreator nodes to match the same template, we must
                            // be able to determine the list of template arguments such that
                            // whenever the template arguments have the same value,
                            // the body formulas of the two nodes have the same value _for each
                            // setting of the quantified variables declared in these nodes_.
                            // That's not the case above: e.g. for x=y={A0}, F(x) is F({A0}) while
                            // F(y.next) is F({A1}).
                            
                            // We can do that by doing template detection on the template arguments.
                            // We allocate a TemplateDetectVisitor for each Template whose instances
                            // are VarCreator nodes.  Suppose we have a particular VarCreator node
                            // that is either the first VarCreator node for this Template, or not
                            // the first but has an identical declaration list to all previously seen
                            // instances of this Template, and has a body formula that
                            // matches the same Template as the body formulas of all previously
                            // seen instances of the Template.  We apply the
                            // Template's TemplateDetectVisitor to the template arguments of the
                            // TemplateInstance computed for the body formula; we tell the TemplateDetectVisitor
                            // to treat quantified variables declared in node_ as non-constant-valued
                            // expressions such that corresponding quantified variables have the same LeafId --
                            // i.e. the i'th quantified variable in each instance of the Template has
                            // the same LeafId for the purposes of this template detection.
                            
                            TemplateInstance bodyTemplateInstance =
                                _getInst(varCreator.getBody());
                            TemplateInstance instTemplateInstance =
                                _getInst(((VarCreator)candTemplNode).getBody());
                            Dbg.check(bodyTemplateInstance.template ==
                                instTemplateInstance.template);
                            Dbg.check(bodyTemplateInstance.args.size() ==
                                instTemplateInstance.args.size());
                            for (int argNum = 0; completeMatch && argNum < bodyTemplateInstance.args.size(); argNum++) {
                                Expr nodeBodyArg = (Expr)bodyTemplateInstance.args.get(argNum);
                                Expr instBodyArg = (Expr)instTemplateInstance.args.get(argNum);
                                TemplateDetectVisitor argTemplDetector = new TemplateDetectVisitor(_translator);
                                argTemplDetector._isAuxiliary = true;
                                argTemplDetector._leafIdSubst = leafIdSubst;
                                argTemplDetector._declaredVarIds = new TreeSet();
                                argTemplDetector._declaredVarIds.addAll(leafIdSubst.keySet());
                                argTemplDetector._declaredVarIds.addAll(leafIdSubst.values());
                                if (_interruptInProgress) return null;
                                TemplateInstance nodeArgTemplInst = _chooseInst(nodeBodyArg.applyReturnVisitor(argTemplDetector));
                                if (_interruptInProgress) return null;
                                TemplateInstance instArgTemplInst = _chooseInst(instBodyArg.applyReturnVisitor(argTemplDetector));
                                if (_interruptInProgress) return null;
                                if (nodeArgTemplInst.template !=
                                    instArgTemplInst.template) {
                                    completeMatch = false;
                                    //              System.out.println("incomplete match: " + node_.fullString() +
                                    //                         " to " + candTemplNode.fullString());
                                    //              System.out.println("nodeArg: " + nodeArgTemplInst.node.fullString() +
                                    //                         " " + nodeArgTemplInst.args);
                                    //              System.out.println("instArg: " + instArgTemplInst.node.fullString() +
                                    //                         " " + instArgTemplInst.args);
                                }
                            }  // loop over template args
                        }  // node_ and template instance declarations are identical up to a renaming
                    }  // special checks for VarCreator nodes
                    
                    /* node_ matches candTempl */
                    if (completeMatch) {
                        Dbg.check(templInst.args.size() == candTemplInst.args.size());
                        // System.out.println("complete match: " + node_.fullString());
                        // System.out.println("       to node: " + candTemplInst.node.fullString());
                        // System.out.println("     with args: " + templInst.args);
                        templInst.template = candTempl;
                        candTempl.instances.add(templInst);
                        matchingTemplateFound = true;
                    }
                    //System.out.println("matched node template: " + node_.fullString()
                    //		   + " with args=" + templInst.args);
                }  // childrenMatch
            }  // loop over candidate templates
        }
        
        if (!matchingTemplateFound) {
            // System.out.println("new node template: " + node_.fullString()
            //             + " with args=" + templInst.args);
            /* Create a new template */
            Template newTempl = new Template();
            _allTemplates.add(newTempl);
            templInst.template = newTempl;
            newTempl.instances.add(templInst);
            
            /* For each child, look at its template, and
             record the fact that its template is a child
             of newTempl. */
            newTempl.children = new Template[childTempl.length];
            for (int i=0; i<childTempl.length; i++) {
                newTempl.children[i] = childTempl[i].template;
                childTempl[i].template.parents.add(newTempl);
            }
        }
        
        //      System.out.println("result for node " + node_.fullString() + " is template "
        //                 + _allTemplates.indexOf(templInst.template) +
        //                 " with args " + templInst.args);
        if (false && (commuteArgs != null)) {
            TemplateInstance commuteTemplInst =
                new TemplateInstance(node_);
            commuteTemplInst.template = templInst.template;
            commuteTemplInst.setArgs(commuteArgs);
            templInst.template.instances.add(commuteTemplInst);
            Dbg.info("commute: " + node_.fullString());
        }
        _chkInst(templInst);
        return Collections.singleton(templInst);
    }  // visit(Node)
    
    //////////////////////////////////////////////////////////////////////////////////////////////
    
    // The following functions are called _after_ the TemplateDetectVisitor has visited
    // all the nodes, to do some postprocessing and to transfer the information gathered
    // about templates to the {@link BooleanFormula}s within {@link Transl}ations of
    // AST {@link Node}s.
    
    public Map getNodeTemplates() { return _node2templateInstance; }
    
    /**
     * Return a {@link List}, possibly with duplicates, of {@link VariableExpr quantified variables} used in a
     * {@link Node}.  Used by {@link #_shortenTemplateArgLists} and by {@link #_updateArgValInfo}.
     */
    private List /* of VariableExpr */ _quantVarsUsedIn(Node node_) {
        if (node_ instanceof VariableExpr &&
                ((VariableExpr)node_).isQuantified)
            return Arrays.asList(new Node[]{node_});
        List quantVarList = new ArrayList();
        for (Iterator childIter = node_.getChildren(); childIter.hasNext();) {
            quantVarList.addAll(_quantVarsUsedIn((Node)childIter.next()));
        }
        return quantVarList;
    }
    
    /**
     * Return a {@link List}, possibly with duplicates, of {@link VariableExpr quantified variables} used in a
     * {@link Node}.  Used by {@link #_shortenTemplateArgLists} and by {@link #_updateArgValInfo}.
     */
    private List /* of VariableExpr */ _freeVarsUsedIn(Node node_) {
        if (node_ instanceof VariableExpr &&
                ((VariableExpr)node_).isQuantified)
            return Arrays.asList(new Node[]{node_});
        List quantVarList = new ArrayList();
        
        Set declaredVarIds = new TreeSet();
        if (node_ instanceof VarCreator) {
            // compute the set of LeafIds of quantified variables declared
            // in the VarCreator
            for (DeclIter declIter = new DeclIter((VarCreator)node_); declIter.hasNext();) {
                declIter.next();
                declaredVarIds.add(declIter.getLeafId());
            }
        }
        
        for (Iterator childIter = node_.getChildren(); childIter.hasNext();) {
            List fvarList = _freeVarsUsedIn((Node)childIter.next());
            for (Iterator varIter = fvarList.iterator(); varIter.hasNext();) {
                VariableExpr varExpr = (VariableExpr)varIter.next();
                if (!declaredVarIds.contains(varExpr.getLeafId()))
                    quantVarList.add(varExpr);
            }
        }
        return quantVarList;
    }
    
    /** Post-processing step to shorten template argument lists
     by removing duplicate arguments.  Once we've visited the entire
     AST and know all instances of each templates, we can try to shorten
     the argument lists of template instances as follows.
     If in every instance of a template T(a,b), the actual arguments
     for a and b are always the same {@link Expr}, i.e. every use
     of T looks like T(a,a), then we can make T a template of just
     one argument. */
    private void _shortenTemplateArgLists() {
        //  System.out.println("[BEFORE SHORTENING:]");
        //  showTemplates();
        //  System.out.println("[[[[[[[[[[[[[]]]]]]]]]]]]]");
        
        for (Iterator templIter = _allTemplates.iterator(); templIter.hasNext();) {
            Template templ = (Template)templIter.next();
            
            //
            // We do shortening in three passes, using three different ways.
            //
            
            // Pass 1:
            
            // If a given argument is the same constant (not constant-valued) expression
            // in all instances, e.g. ^next, then we can drop the argument from all instances,
            // because it is always going to match.
            
            {
                int numArgs = templ.getNumArgs();
                List argsToKeep = new ArrayList(); // of Integer
                for (int formalArg = 0; formalArg < numArgs; formalArg++) {
                    Expr firstArg = null;
                    boolean keepArg = false;
                    for (Iterator instIter = templ.instances.iterator();
                    !keepArg && instIter.hasNext();) {
                        TemplateInstance inst = (TemplateInstance)instIter.next();
                        Expr arg = (Expr)inst.args.get(formalArg);
                        Transl transl = _translator.getNodeTransl(arg);
                        if (!transl.isConstant())
                            keepArg = true;
                        else {
                            if (firstArg == null)
                                firstArg = arg;
                            else
                                if (!arg.isSameAs(firstArg))
                                    keepArg = true;
                        }
                    }
                    if (keepArg)
                        argsToKeep.add(new Integer(formalArg));
                }
                templ.keepOnlyArgs(argsToKeep);
            }
            
            // Pass 2:
            
            // If a given argument is the same constant-valued expression in all instances,
            // e.g. x.next, we can replace it with just a flat list of the free quantified variables
            // used in the expression, because they completely determine the value of the
            // argument: x.next can be replaced by just x if x is a quantified variable.
            // This pass may enable the next pass (duplicate argument removal) to do more
            // simplification.
            
            {
                //int numArgs = templ.getNumArgs();
                for (int formalArgNum = 0; formalArgNum < templ.getNumArgs(); formalArgNum++) {
                    // Determine whether in all TemplateInstances of this Template,
                    // formalArgNum'th argument is the same expression.
                    
                    Expr firstArg = null;
                    boolean foundDiff = false;
                    for (Iterator instIter = templ.instances.iterator();
                    !foundDiff && instIter.hasNext();) {
                        TemplateInstance inst = (TemplateInstance)instIter.next();
                        Expr arg = (Expr)inst.args.get(formalArgNum);
                        Transl transl = _translator.getNodeTransl(arg);
                        if (firstArg == null)
                            firstArg = arg;
                        else
                            if (!arg.isSameAs(firstArg))
                                foundDiff = true;
                    }
                    
                    if (!foundDiff && !(firstArg instanceof VariableExpr)) {
                        // In every TemplateInstance of this Template, replace this argument
                        // with a list of quantified variables used in the argument.
                        // This should increase opportunities for elimination of duplicates
                        // in the next pass.
                        
                        //          System.out.println("--->shortening arg: " + formalArgNum);
                        //          if (templ.instances.size() > 1) {
                        //              TemplateInstance inst1 = (TemplateInstance)templ.instances.get(0);
                        //              TemplateInstance inst2 = (TemplateInstance)templ.instances.get(1);
                        //              Expr arg1 = (Expr)inst1.args.get(formalArgNum);
                        //              Expr arg2 = (Expr)inst2.args.get(formalArgNum);
                        //              Dbg.check(arg1.isSameAs(arg2));
                        //          }
                        
                        //          for (Iterator instIter = templ.instances.iterator(); instIter.hasNext();) {
                        //              TemplateInstance inst = (TemplateInstance)instIter.next();
                        //              System.out.println(inst.args);
                        //          }
                        //          System.out.println("--->");
                        
                        for (Iterator instIter = templ.instances.iterator(); instIter.hasNext();) {
                            TemplateInstance inst = (TemplateInstance)instIter.next();
                            Expr arg = (Expr)inst.args.get(formalArgNum);
                            List replaceList = inst.args.subList(formalArgNum, formalArgNum+1);
                            replaceList.clear();
                            replaceList.addAll(_freeVarsUsedIn(arg));
                        }
                    }
                }  // loop over formal args
            }  // pass 2
            
            // Pass 3:
            
            // If in every instance of a template T(a,b), the actual arguments
            // for a and b are always the same {@link Expr}, i.e. every use
            // of T looks like T(a,a), then we can make T a template of just
            // one argument.
            
            // all instances of templ have the same number of arguments.
            // here we compute the indices of those arguments that
            // we should keep.
            {
                int numArgs = templ.getNumArgs();
                if (numArgs < 2) continue;
                List argsToKeep = new ArrayList(); // of Integer
                argsToKeep.add(new Integer(0));
                for (int formalArg = 1; formalArg < numArgs; formalArg++) {
                    // for each earlier argument, test whether in ALL instantiations
                    // of the template, formalArg is the
                    // same as that earlier argument.
                    boolean sameAsAnEarlier = false;
                    for (int earlierArg = 0; !sameAsAnEarlier && earlierArg < formalArg; earlierArg++) {
                        boolean sameAsThisEarlier = true;
                        for (Iterator instIter = templ.instances.iterator();
                        sameAsThisEarlier && instIter.hasNext();) {
                            TemplateInstance templInst = (TemplateInstance)instIter.next();
                            Dbg.check(templInst.args.size() == numArgs);
                            Expr formalArgExpr = (Expr)templInst.args.get(formalArg);
                            Expr earlierArgExpr = (Expr)templInst.args.get(earlierArg);
                            if (!formalArgExpr.isSameAs(earlierArgExpr))
                                sameAsThisEarlier = false;
                        }   // loop over template instantiations
                        if (sameAsThisEarlier)
                            sameAsAnEarlier = true;
                    }  // loop over earlier args, checking if any always matches formalArg
                    if (!sameAsAnEarlier)
                        argsToKeep.add(new Integer(formalArg));
                }  // loop over formal args, looking for ones to drop
                
                // Keep only those args we'd like to keep
                templ.keepOnlyArgs(argsToKeep);
            }
        }  // loop over templates
    }  // shortenTemplateArgLists
    
    /** Pass the knowledge of shared AST subformulas to the {@link BooleanFormula}
     generated from translation.
     <p>
     At this point, each {@link Node}, including nodes that are the template instances,
     has been {@link alloy.transl translated} into a {@link Transl}.  For a given template,
     all of its instances translate into a {@link Transl} of the same class and scope(s).
     Each {@link Transl} can be viewed as an array of {@link BooleanFormula}s.
     For any two instances of the same template, if template parameters on the two instances evalute
     to the same sequence of constant {@link Expr} values (based on the current values
     of the {@link alloy.bool.BoolSwitch switches}), the corresponding {@link Transl}s
     represent the same {@link alloy.util.MultiDimArray arrays} of {@link BooleanFormula}s.
     That means the corresponding
     elements of the two arrays -- the corresponding {@link BooleanFormula}s in the two
     same-class, same-scope {@link Transl}s -- represent the same Boolean functions.
     We record this information on the {@link BooleanFormula}s, marking corresponding
     {@link BooleanFormula}s with the same {@link BooleanFormula#templCacheId} value.
     E.g. if a template represents a set over a {@link alloy.type.BasicType} of
     {@link alloy.type.BasicType#getScope scope} 3, each instance of
     that template translates to an array of 3 {@link BooleanFormula}s;
     we write the same ID to the 0'th {@link BooleanFormula} in each of these arrays,
     another ID to the 1st {@link BooleanFormula} in each of these arrays, and
     another ID to the 2nd {@link BooleanFormula} in each of these arrays.
     So, the 0'th elements of the denotations translated from instances of the same
     template correspond to each other, and so do the 1st elements, and the 2nd.
     For each template, we create a range of cache IDs, one cache ID for each
     array index in the denotation, and write that cache ID to the {@link BooleanFormula#templCacheId}
     field of {@link BooleanFormula}s stored
     at that array index in denotations translated from instances of the template.
     <p>
     Writes: {@link BooleanFormula#templCacheId}, {@link BooleanFormula#templCacheKey},
     {@link BooleanFormula#templArgScopes}.
     */
    private void _markSharedBooleanFormulas() {
        int curCacheId = 1;
        Dbg.info("Detecting shared subformulas...");
        // Loop over templates
        for (Iterator templIter = _allTemplates.iterator(); templIter.hasNext();) {
            Template templ = (Template)templIter.next();
            
            if (_interruptInProgress) return;
            
            if (templ.getAnInstance().node instanceof Leaf) continue;
            if (_isConstantValued(templ.getAnInstance().node)) continue;
            if (_relTypeTemplate.containsValue(templ) ||
                    _leafTemplate.containsValue(templ))
                continue;
            
            // Save the cache ID at the beginning of the cache ID range
            // allocated to template templ.
            int saveCacheId = curCacheId;
            // Loop over instances of template templ
            for (Iterator instIter = templ.instances.iterator(); instIter.hasNext();) {
                TemplateInstance templInst = (TemplateInstance)instIter.next();
                // reset template ID counter to the beginning of the range
                // for the current template (templ)
                curCacheId = saveCacheId;
                
                List argList = new ArrayList();
                int[] argScopes = new int[templInst.args.size()];
                int argNum = 0;
                for (Iterator argIter = templInst.args.iterator();
                argIter.hasNext();) {
                    if (_interruptInProgress) return;
                    Node arg = (Node)argIter.next();
                    Transl argTransl = _translator.getNodeTransl(arg);
                    Dbg.check(argTransl);
                    List argTranslFormulas = argTransl.getBooleanFormulas();
                    argScopes[argNum++] = argTranslFormulas.size();
                    argList.addAll(argTranslFormulas);
                }
                
                _chkInst(templInst);
                
                Transl templTransl = _translator.getNodeTransl(templInst.node);
                Dbg.check(templTransl);
                for (Iterator boolIter = templTransl.getBooleanFormulas().iterator();
                boolIter.hasNext();) {
                    if (_interruptInProgress) return;
                    BooleanFormula boolFormula = (BooleanFormula)boolIter.next();
                    int[] templArgMults = new int[argScopes.length];
                    for (int i=0; i<argScopes.length; i++)
                        templArgMults[i] = ((Integer)templ.argMults.get(i)).intValue();
                    if (false) {
                        System.out.println("curCacheId: " + curCacheId);
                        System.out.println("node: " + templInst.node.pp());
                        System.out.println("inst args: " + templInst.args);
                        System.out.println("bool args: " + argList);
                        System.out.println("mults: " + Util.str(templArgMults));
                    }
                    boolFormula.recordCachingInfo(curCacheId++,
                            (BooleanFormula[])argList.toArray(new BooleanFormula[]{}),
                            argScopes,
                            templArgMults);
                }
            }
        }
        Dbg.info("Detected shared subformulas.");
    }
    
    //private Formula _saveFormula;
    
    public void preprocess(Formula f_) {
        // _saveFormula = f_;
    }
    
    public void postprocess() {
        if (_interruptInProgress) return; 
        _shortenTemplateArgLists();
        if (_interruptInProgress) return;
        _determineArgMults();
        if (_interruptInProgress) return;
        _markSharedBooleanFormulas();
    }
    
    /** Determine argument multiplicities for each template. */
    private void _determineArgMults() {
        //Dbg.info("Determining arg multiplicities...");
        for (Iterator templIter = _allTemplates.iterator(); templIter.hasNext();) {
            if (_interruptInProgress) return;
            Template templ = (Template)templIter.next();
            templ.argMults = new ArrayList();
            for (int argPos = 0; argPos < templ.getNumArgs(); argPos++) {
                int mult = BooleanFormula.MULT_SCALAR;
                for (Iterator instIter = templ.instances.iterator(); instIter.hasNext();) {
                    TemplateInstance templInst = (TemplateInstance)instIter.next();
                    Expr arg = (Expr)templInst.args.get(argPos);
                    mult = _updateArgValInfo(arg, mult);
                    //          if (arg.pp().indexOf("LegalTrans@s . ")!=-1) {
                    //          System.out.println("arg=" + arg.pp());
                    //          System.out.println("mult=" + _mult2str(mult));
                    //          }
                    if (mult == BooleanFormula.MULT_SET)
                        break;
                }
                templ.argMults.add(new Integer(mult));
            }
        }
        //Dbg.info("Determined arg multiplicities.");
    }
    
    private static String _mult2str(int mult) {
        switch(mult) {
        case BooleanFormula.MULT_SET: return "set";
        case BooleanFormula.MULT_SCALAR: return "scalar";
        case BooleanFormula.MULT_OPTION: return "option";
        default: return "unknown";
        }
    }
    
    /**
     * Immediately interrupt the template detection process, and return.
     * This is called if the user manually interrupts analysis.
     */
    public void interrupt() {
        _interruptInProgress = true;
    }
    
    
    /** Print the templates we've detected, for debugging purposes only. */
    public void showTemplates() {
        List templates = new ArrayList(_allTemplates);
        Collections.sort(templates,
                new Comparator() {
            public int compare(Object obj1_, Object obj2_) {
                Template t1 = (Template)obj1_;
                Template t2 = (Template)obj2_;
                Integer i1 = new Integer(t1.getAnInstance().args.size());
                Integer i2 = new Integer(t2.getAnInstance().args.size());
                return i1.compareTo(i2);
            }
        });
        
        
        
        System.out.println("========= Templates ============");
        for (Iterator templIter = templates.iterator(); templIter.hasNext();) {
            Template templ = (Template)templIter.next();
            System.out.println("-----------------------------");
            System.out.println(templ.argMults);
            for (Iterator instIter = templ.instances.iterator(); instIter.hasNext();) {
                TemplateInstance templInst = (TemplateInstance)instIter.next();
                System.out.println(/*templInst.node.fullString() + */" args=" + templInst.args);
            }
            
        }
        System.out.println("================================");
    }
    
    /**
     * Determine some info on the possible values of the given template instance argument
     * during grounding-out.  We determine whether the given constant-valued {@link Expr}
     * can have an empty relation value, and whether it can refer to a multi-tuple relation value.
     * The most common case is that a template instance argument is a single quantified variable
     * that can take on only singleton-tuple relation values.
     *
     * @param arg_ the {@link Expr} from {@link TemplateInstance#args} of some template instance
     *             (but we do not rely on the fact that it is an argument -- just that it is a
     *              constant-valued expression).
     * @param argMult_ currently known argument multiplicity.
     *
     * @return an integer of which the lowest two bits are significant: bit 0 is set iff
     */
    private int _updateArgValInfo(Expr arg_, int argMult_) {
        if (argMult_ == BooleanFormula.MULT_SET)
            return argMult_;  // nothing more to determine
        
        if (arg_ instanceof EmptySetExpr)
            return BooleanFormula.MULT_OPTION;
        
        // check for the most common case: template instance argument
        // consisting of a single quantified variable
        if (arg_ instanceof VariableExpr &&
                ((VariableExpr)arg_).isQuantified) {
            VariableExpr varExpr = (VariableExpr)arg_;
            //
            // Determine from the variable's declaration what
            // kinds of values it can take during grounding-out
            //
            
            LeafId varLeafId = varExpr.getLeafId();
            // variables declared in comprehension expressions always
            // denote singleton-tuple relation values during grounding-out
            if (_translator.getVarCreator(varLeafId) instanceof ComprehensionExpr)
                return _weakestMult(argMult_, BooleanFormula.MULT_SCALAR);  // cannot be empty or multi-tuple
            
            MultiplicityExpr multExpr = _translator.getLeafMultiplicity(((Leaf)arg_).getLeafId());
            if (multExpr instanceof SetMultExpr) {
                Multiplicity mult = multExpr.getMult();
                if      (mult.equals(Multiplicity.SET))  return _weakestMult(argMult_, BooleanFormula.MULT_SET);
                else if (mult.equals(Multiplicity.ONE))  return _weakestMult(argMult_, BooleanFormula.MULT_SCALAR);
                else if (mult.equals(Multiplicity.LONE)) return _weakestMult(argMult_, BooleanFormula.MULT_OPTION);
                else if (mult.equals(Multiplicity.NONE)) return _weakestMult(argMult_, BooleanFormula.MULT_SCALAR);
                else {
                    Dbg.check(false, "missing set multiplicity");
                    return BooleanFormula.MULT_SET;
                }
            } else // relation multiplicity
                return _weakestMult(argMult_, BooleanFormula.MULT_SET);
        } else {  // !(arg_ instanceof VariableExpr)
            //
            // Evaluate arg_ for all possible combinations of values
            // of the quantified variables on which the arg_ depends.
            //
            
            //System.out.println("arg=" + arg_.nodeString());
            
            // get the list of quantified variables on which arg_'s value
            // depends
            List quantVars = _freeVarsUsedIn(arg_);
            
            //System.out.println("free vars: " + quantVars);
            
            // eliminate duplicates
            Set leafIdSet = new TreeSet();
            for (Iterator quantVarIter = quantVars.iterator(); quantVarIter.hasNext();)
                leafIdSet.add(((Leaf)quantVarIter.next()).getLeafId());
            
            quantVars = new ArrayList(leafIdSet);
            
            // cycle through all possible value combinations of the quantified
            // variables in quantVars.
            
            QVarIterationInfo[] quantVarInfo = new QVarIterationInfo[quantVars.size()];
            int[] quantVarRangeSizes = new int[quantVarInfo.length];
            for (int i=0; i<quantVars.size(); i++) {
                LeafId leafId = (LeafId)quantVars.get(i);
                //System.out.println("leafId: " + _translator.getLeafRep(leafId).nodeString());
                quantVarInfo[i] = _translator.getQVarIterationInfo(leafId);
                quantVarRangeSizes[i] = quantVarInfo[i].getBoolSwitchValues().length;
            }
            
            Transl transl = _translator.getNodeTransl(arg_);
            List boolFormulas = transl.getBooleanFormulas();
            for (MultiDimIter multiIter = new MultiDimIter(quantVarRangeSizes); multiIter.hasNext();) {
                int[] boolSwitchChoices = (int[])multiIter.next();
                // set the boolean switches to the current combination of quantified variable values
                for (int i=0; i<boolSwitchChoices.length; i++) {
                    quantVarInfo[i].getBoolSwitch().setVarValue(quantVarInfo[i].getBoolSwitchValues()[boolSwitchChoices[i]]);
                }
                // count the number of true tuples in arg for the current combination of quantified variable avlues
                int numTuples = 0;
                for (Iterator boolFormIter = boolFormulas.iterator(); boolFormIter.hasNext();) {
                    BooleanFormula bf = (BooleanFormula)boolFormIter.next();
                    if (bf.interpret())
                        numTuples++;
                    if (numTuples > 1) {
                        for (int i=0; i<boolSwitchChoices.length; i++)
                            quantVarInfo[i].getBoolSwitch().clearVarValue();
                        return BooleanFormula.MULT_SET;
                    }
                }
                for (int i=0; i<boolSwitchChoices.length; i++)
                    quantVarInfo[i].getBoolSwitch().clearVarValue();
                if (numTuples == 0)
                    argMult_ = _weakestMult(argMult_, BooleanFormula.MULT_OPTION);
            }
            return argMult_;
        }  // arg_ not just a quantified variable
    }  // _updateArgValInfo()
    
    private static int _weakestMult(int oldMult_, int newMult_) {
        if (oldMult_ == BooleanFormula.MULT_SET ||
                newMult_ == BooleanFormula.MULT_SET)
            return BooleanFormula.MULT_SET;
        if (oldMult_ == BooleanFormula.MULT_OPTION ||
                newMult_ == BooleanFormula.MULT_OPTION)
            return BooleanFormula.MULT_OPTION;
        Dbg.check(oldMult_ == BooleanFormula.MULT_SCALAR &&
                newMult_ == BooleanFormula.MULT_SCALAR);
        return BooleanFormula.MULT_SCALAR;
    }
    
    
    /**
     * Check that each argument in {@link TemplateInstance#args} refers only
     * to quantified variables declared above {@link TemplateInstance#node}.
     */
    private void _chkInst(TemplateInstance templInst_) {
        for (Iterator argIter = templInst_.args.iterator(); argIter.hasNext();) {
            Node arg = (Node)argIter.next();
            Dbg.check(_isConstantValued(arg));
            List quantVars = _freeVarsUsedIn(arg);
            //System.out.println("arg: " + arg.fullString());
            for (Iterator quantVarIter = quantVars.iterator(); quantVarIter.hasNext();) {
                LeafId leafId = ((VariableExpr)quantVarIter.next()).getLeafId();
                //System.out.println(" free: " + _translator.getVariable(leafId).fullString());
                VarCreator declaredAt = _translator.getVarCreator(leafId);
                Dbg.check(_translator.isAncestor(declaredAt, templInst_.node));
            }
        }
    }
    
    /** Take a {@link Set} of {@link TemplateInstance}s, and return one of them. */
    private TemplateInstance _chooseInst(Object instSet_) {
        if (_interruptInProgress) return null;
        return (TemplateInstance)((Set)instSet_).iterator().next();
    }
    
    /**
     * @return the {@link TemplateInstance} computed for a previously visited
     *         {@link Node}.
     */
    private TemplateInstance _getInst(Node n_) {
        return _chooseInst(_node2templateInstance.get(n_));
    }
    
}  // class TemplateDetectVisitor
